$\forall$$T$:Type, $P$:($T$$\rightarrow$Prop), $x$:\{$t$:$T$$\mid$ $P$($t$) \}, $a$:Atom1.
\\[0ex]AtomFree(Type;$T$) $\Rightarrow$ AtomFree($T$$\rightarrow$Prop;$P$) $\Rightarrow$ $x$:$T$$>>$$a$ $\Rightarrow$ $x$:\{$t$:$T$$\mid$ $P$($t$) \}$>>$$a$